Z3: handle exceptions from Z3 in a few more places. #408
Conversation
If Z3 is interrupted at those places, we throw a InterruptedException. We remove the solver-specific Z3SolverException. It does not bring any benefit over a default SolverException. This fixes #406.
There was a problem hiding this comment.
Sneakily throwing a checked exception without declaring is technically possible in Java, but do you really want that?
Inside an application where all the code is under control and one knows what will happen if a specific exception is thrown this can be ok. But in the public API of a library I would say that this is really bad style. You would have to extensively document which exceptions can be thrown in which cases, and all of your users would have to manually take care to properly handle all of them in all cases, which will be really tedious. I think it is obvious that for much calling code this will just not happen.
As a user of a library I would find such a strategy highly fishy and it would make me question whether I really want to use that library unless there are very good reasons for this. Think of the image and reputation that this good give JavaSMT in the long term.
You are also doing this for both InterruptedException and SolverException, but I think these two cases should be discussed separately.
InterruptedException could be considered one of the more benign cases. For many users it will never happen (because they never cancel the solver), and for those who do, it might be the case that they have high-level handling of it somewhere that will catch all cases of it being thrown anyway (that is the situation in CPAchecker, for example). And the cases where InterruptedException might be thrown are clearly defined and easy to understand. But on the other hand, for InterruptedException is also less important to be thrown at all, because there is the alternative strategy of setting the current thread's interrupted flag, so why bother with hacking around Java's type system?
For SolverException, however, I think it is not clear that users can know whether to expect this exception, nor that it is clearly defined and easy to understand when and why it happens, nor what to do once it has happened. So application code will likely not be in a situation where they can handle this as well as InterruptedException. So I would be even more scared by this exception to be thrown from arbitrary places than for InterruptedException.
And of course all this raises the question whether you really want this precedence. If you add it here, do you think it will stop here, or will similar cases be added to JavaSMT whenever a similar problem arises?
|
|
||
| import org.sosy_lab.java_smt.api.SolverException; | ||
|
|
||
| /** This exception is thrown by native Z3 code, through our customized JNI bindings. */ |
There was a problem hiding this comment.
It seems the bindings need to be fixed as well.
There was a problem hiding this comment.
There is no need to update anything. Since several years, JavaSMT relies on the original JNI bindings directly from Z3. This exception was never thrown from there. This class was taken over from CPAchecker in 2015, and it was never really used.
If Z3 is interrupted at those places, we throw a InterruptedException.
We remove the solver-specific Z3SolverException.
It does not bring any benefit over a default SolverException.
This fixes #406.